Repository navigation
Model the spawn-coherence relation: producer-absence and never-observed are different states - #9268
Merged
Merged
Conversation
…Evaluated, never to agreement THE SUBJECT IS ONE SPAWN, NOT ONE JOB. A job that spawns rustfmt eleven times has eleven opportunities to exec different bytes, so a job-grained receipt would report a coherence it never established. The digest is taken at spawn and travels with the observation rather than being resolved once and looked up later, because resolving a pathname and re-launching it afterwards is the defect the carrier exists to detect. THREE CAUSES, NOT COLLAPSED. "we could not tell" and "we checked and they differed" have opposite remedies, so ToolchainIdentitiesDiffered is a finding beside NotEvaluated rather than inside it. Cross-family comparison is its own cause because std.content_hash refuses to collapse an fnv1a64 fingerprint against a sha256 digest: reporting that as "differed" would manufacture a finding, reporting it as "equal" would manufacture a pass. WHAT THIS IS NOT. It does not nickname ObservedToolIdentityDuplicate. That arm folds one ResolvedBuildContext roster and carries only a `count`, discarding the identities, so it cannot answer whether the duplicates agreed -- it is a name-multiplicity fact over one snapshot, where this is a byte-agreement fact over a spawn sequence. RUNG, STATED HONESTLY: NOTHING CONSTRUCTS A ToolchainSpawn YET. No producer observes spawns, so the carrier's live answer today is ToolchainNeverObserved, and it says so rather than reporting agreement. This is a modeled domain type landing ahead of its producer, not a closed loop, and it must not be cited as coverage that successive spawns reached the same bytes -- they are unmeasured. Four witnesses, executed green via claim_batch --hermetic. The discriminating red is differing_bytes_mid_run_is_a_finding: one pass reaching different bytes must return a finding, not NotEvaluated. The empty-list arm is asserted first and deliberately -- if it ever returns Single, absence of evidence has started rendering as a pass. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…erved, and carry the grain that picks the remedy Operator ruling: land this as a standalone model-only PR, do not serialize the session-capacity program behind it. The ruling set a merge bar; three of its conditions already held (no authored population passed off as a production read, no Bool collapse of the outcomes, no producer). Three did not. 1. PRODUCER-ABSENT IS NOT NEVER-OBSERVED. The fold returned ToolchainNeverObserved for an empty list, so the first producer wired to this carrier would have rendered its OWN ABSENCE as "we checked and found no comparable pair". That is the execution-provenance loss DESIGN names -- a masked run and a clean run rendering identically. SpawnObservationProducerAbsent is now its own cause. The fold cannot RETURN it, and that is correct rather than a dead arm: a fold speaks only about the list it was handed, while producer absence is a claim about the world that only a declaration or a real observation transaction may make. 2. THE GRAIN COULD NOT PICK THE REMEDY. ToolchainSpawn carried no resolved executable and no spawn identity, so two spawns diverging at ONE path (the binary was replaced under us) and two spawns diverging at DIFFERENT paths (we ran two different binaries) collapsed into one verdict. They have opposite repairs. The Differed arm now carries both spawns. std.types.FilePath is reused rather than minting a path type. 3. THE NEXT-RUNG TRIGGER IS A SEAM, NOT "OBSERVE LATER". The disposition names what a spawn must emit and where the producer belongs -- the shared spawn/execution substrate the aggregate-demand instrument will also read, not a capacity-only producer, which would give this fact a second home. WHAT THIS PR DOES NOT CLAIM, stated plainly because the ruling turns on it: no production spawn has been observed, no host is established to have used the same executable twice, and toolchain coherence is NOT guaranteed by anything here. The carrier classifies observations it is given. Nothing gives it any. The witnesses establish the classifier's distinctions and nothing about any host. Six witnesses via claim_batch --hermetic, all PASS, two of them new: producer_absent_is_not_never_observed pins the split in (1); divergence_carries_the_paths_that_pick_the_remedy asserts (2) in both directions, so the evidence does the work rather than the arm's name. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds
gunbc.toolchain_coherence: the relation by which spawn observations are classified as coherent, divergent, or unevaluated. Model-only, by operator ruling.The question it answers is not
digest A == digest B. It is: two spawns claiming to inhabit one tool role, inside one pass, reached the same executable bytes. The subject is ONE SPAWN, not one job — a job that spawns rustfmt eleven times has eleven opportunities to exec different bytes, so a job-grained receipt would report a coherence it never established. The digest is taken at spawn and travels with the observation, because resolving a pathname and re-launching it afterwards is precisely the defect the carrier exists to detect.What this PR does NOT claim
Stated first, because the ruling turns on it:
The relation is terminal; its production standing is a stall.
gunbc_toolchain_coherence_dispositionrecords both, so the declaration is not named as though coherence had been achieved (DESIGN §4b(1) rung inflation).Three states the design turns on
SpawnObservationProducerAbsent≠ToolchainNeverObserved. Before this split the fold returnedNeverObservedfor an empty list, so the first producer wired to the carrier would have rendered its own absence as "we checked and found no comparable pair" — the execution-provenance loss DESIGN names, where a masked run and a clean run render identically.NeverObservedis now reserved for an observation transaction that RAN and found no comparable pair. The fold cannot returnProducerAbsent, which is correct rather than a dead arm: a fold speaks only about the list it was handed; producer absence is a claim about the world.ToolchainIdentityIncomparableis its own cause.std.content_hashrefuses to collapse a cross-family pair. Reporting that as "differed" would manufacture a finding; reporting it as "equal" would manufacture a pass.Differedis a finding besideNotEvaluated, never inside it. "We could not tell" and "we checked and they differed" have opposite remedies. No outcome projects toBool.Grain: the finding must pick the remedy
ToolchainSpawncarries pass, spawn identity, slot, resolved executable, and the observed digest. Without the resolved path, two spawns diverging at ONE path (the binary was replaced under us) and at DIFFERENT paths (we ran two different binaries) collapse into one verdict — opposite repairs. TheDifferedarm carries both spawns so the consumer can tell them apart.std.types.FilePathis reused rather than minting a path type.Not a nickname for
ObservedToolIdentityDuplicateThat arm folds one
ResolvedBuildContextroster and carries only acount, discarding the identities — it cannot answer whether the duplicates agreed. It is a name-multiplicity fact over one snapshot; this is a byte-agreement fact over a spawn sequence.Next-rung trigger
A spawn operation emits tool identity, resolved executable, executable digest, pass identity and spawn identity at the moment of spawn; two such observations sharing one tool role within one pass are handed to
toolchain_coherence_of. That producer belongs to the shared spawn/execution substrate the aggregate-demand instrument will also read — not a capacity-only producer, which would give this fact a second home.Test plan
claim_batch --source-root dag --source-root src/v2 --hermetic --entry dag/test/claim/toolchain_coherence_witness_test.dag— 6/6 PASS:no_observation_is_not_evaluatedNotEvaluated, never agreementsame_bytes_across_passes_is_singleSinglediffering_bytes_mid_run_is_a_findingNotEvaluatedone_spawn_is_singleproducer_absent_is_not_never_observeddivergence_carries_the_paths_that_pick_the_remedyFocused green is preflight; required CI is the completion receipt. The witnesses establish the classifier's distinctions and nothing about any host.